Nuprl Definition : es-bact 0,22

action[[a n]][e1;e2]
== Case TERMOF{decidable ecl-es-act:ObjectId, 1:l, i:l}(ds,da,a,es,loc(e1),x.*,x,y. *,n,e1,e2) of
== inl(x)  true
== inr(x)  false 
latex



clarification:

es-bact{i:l}
es-bact(ds; da; a; es; n; e1; e2)
== Case TERMOF{decidable ecl-es-act:ObjectId, 1:l, i:l}
== Case (ds
== Case ,da
== Case ,a
== Case ,es
== Case ,es-loc(es; e1)
== Case ,x.*
== Case ,x,y. *
== Case ,n
== Case ,e1
== Case ,e2) of
== inl(x)  true
== inr(x)  false 
latex


Definitionsaction[[a n]][e1;e2], decidable ecl-es-act, loc(e), true, false
FDL editor aliaseses-bact

origin